$\forall$$T$:Type, ${\it as}$,${\it as'}$,${\it bs}$,${\it cs}$:($T$ List).
\\[0ex]($\parallel$${\it as}$$\parallel$ = $\parallel$${\it as'}$$\parallel$ $\in$ $\mathbb{Z}$) $\Rightarrow$ (append(${\it as}$; ${\it cs}$) = append(${\it as'}$; ${\it bs}$) $\in$ ($T$ List)) $\Rightarrow$ (${\it cs}$ = ${\it bs}$)